Skip to content

feat(Algebra/Homology/SpectralObject): HasSpectralSequence#35374

Open
joelriou wants to merge 11 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-2-has-spectral-sequence
Open

feat(Algebra/Homology/SpectralObject): HasSpectralSequence#35374
joelriou wants to merge 11 commits intoleanprover-community:masterfrom
joelriou:spectral-sequences-2-has-spectral-sequence

Conversation

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Feb 15, 2026
@github-actions
Copy link

PR summary 99884c2730

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (new file) 101
Mathlib.Order.Fin.Clamp (new file) 342
Mathlib.Algebra.Homology.SpectralObject.Basic (new file) 781
Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence (new file) 786

Declarations diff

+ HasSpectralSequence
+ Hom
+ SpectralObject
+ SpectralSequenceMkData
+ composableArrows₅
+ composableArrows₅_exact
+ epi_H_map_twoδ₁Toδ₀
+ epi_H_map_twoδ₁Toδ₀'
+ exact₁
+ exact₂
+ exact₃
+ instance (E : SpectralObject C EInt) : E.HasSpectralSequence mkDataE₂Cohomological
+ instance : Category (SpectralObject C ι)
+ instance {l : ℕ} (E : SpectralObject C (Fin (l + 1))) :
+ isIso_H_map_twoδ₁Toδ₀
+ isIso_H_map_twoδ₁Toδ₀'
+ isZero_H_map_mk₁_of_isIso
+ isZero_H_obj_mk₁_i₀_le
+ isZero_H_obj_mk₁_i₀_le'
+ isZero_H_obj_mk₁_i₃_le
+ isZero_H_obj_mk₁_i₃_le'
+ i₀_le
+ i₃_le
+ le₀'₀
+ le₀₁'
+ le₁₂'
+ le₂₃'
+ le₃₃'
+ mkDataE₂Cohomological
+ mkDataE₂CohomologicalFin
+ mkDataE₂CohomologicalNat
+ mkDataE₂HomologicalNat
+ mono_H_map_twoδ₁Toδ₀
+ mono_H_map_twoδ₁Toδ₀'
+ sc₁
+ sc₂
+ sc₃
+ spectralSequenceFin
+ spectralSequenceFin_rel_iff
+ spectralSequenceNat
+ spectralSequenceNat_rel_iff
+ zero₁
+ zero₂
+ zero₃
+ δ
+ δ_naturality
+ δ_δ

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 15, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory WIP Work in progress

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

Comments